es:ES, i, x:Id, T:Type, v:T. @i x initially v:T  Prop 

latex

Definitions	b, P  Q, A, False, t  T, x:A. B(x), Id, True, T, ES, vartype(i;x), x when e, loc(e), E, Prop, first(e), x. t(x), e@i. P(e), A & B, @i x initially v:T
Lemmas	alle-at wf, assert wf, es-first wf, es-E wf, es-loc wf, es-when wf, subtype rel wf, es-vartype wf, squash wf, true wf, Id wf, event system wf, es-loc-pred